$\forall$$T$:Type, $L$:($T$ List). ($\neg$($L$ = [])) $\Rightarrow$ (0 $<$ $\parallel$$L$$\parallel$)